#pragma once

#include "clause.h"
#include <list>
#include <algorithm>

namespace solver
{
	class decision
	{
	public:
		int decision_idx;
		int selected_literal;
		std::vector<literal> literals;
	};

	typedef decision *pdecision;

	class decision_char
	{
	public:
		literal lit;
		int decision_idx;
	};

	class decision_string : public std::vector<decision_char>
	{
	public:

		decision_string()
		{
			
		}

		bool contains(decision_string& dec)
		{
			for (auto&ic : *this)
			{
				bool found = false;
				for (auto&ix : dec)
				{
					if (ix.lit == ic.lit)
					{
						found = true;
						break;
					}
				}
				if (!found)
					return false;
			}
			return true;
		}

		void push_back(const decision_char& dc)
		{
			std::vector<decision_char>::push_back(dc);
		}

		bool push_back(literal l, int decision_idx)
		{
			bool success = conflict_free(l);
			if (success) 
			{
				decision_char dc;
				dc.decision_idx = decision_idx;
				dc.lit = l;
				push_back(dc);
			}
			return success;
		}

		bool conflict_free(literal l)
		{
			bool success = true;

			for (auto& v : *this) 
			{
				auto& lv = v.lit;
				if (lv.ref == l.ref && lv.spin != l.spin)
				{
					success = false;
					break;
				}
			}

			return success;
		}

		bool exists_conflict_free(literal l, bool& found)
		{
			bool success = true;
			found = false;
			for (auto& v : *this)
			{
				auto& lv = v.lit;
				if (lv.ref == l.ref)
				{
					found = true;
					success = (lv.spin == l.spin);
					break;
				}
			}

			return success;
		}

		bool conflict_free(pdecision dec)
		{
			int s = dec->literals.size();

			for (auto& dc : dec->literals)
			{
				bool found;
				bool is_free = exists_conflict_free(dc, found);
				if (!found)
					return true;
				if (!is_free)
					return false;
			}

			return true;
		}

		decision_string remove_literal(literal lit)
		{
			decision_string dsx;
			for (auto ch : *this) 
			{
				if (ch.lit != lit) 
				{
					dsx.push_back(ch);
				}
			}
			return dsx;
		}

		decision_string *clone()
		{
			decision_string *ds = new decision_string(*this);
			return ds;
		}

		void sort()
		{
			std::sort(begin(), end(), [](const decision_char& a, const decision_char& b) {
				return a.lit.ref < b.lit.ref;
			});
		}

		static bool compare (const decision_string& srcA, const decision_string& srcB)
		{
			auto srcAi = srcA.begin();
			auto srcBi = srcB.begin();

			while (srcAi != std::end(srcA) && srcBi != std::end(srcB))
			{
				if (srcAi->lit.ref >= srcBi->lit.ref) return false;
				srcAi++;
				srcBi++;
			}

			if (srcAi != std::end(srcA) && srcBi == std::end(srcB))
				return false;

			return true;
		}

		static bool compare(const decision_string* srcA, const decision_string* srcB)
		{
			return compare(*srcA, *srcB);
		}

	};

	typedef decision_string *pdecision_string;

}
